Search for: All records

Post-silicon validation is a vital step in System-on-Chip (SoC) design cycle. A major challenge in post-silicon validation is the limited observability of internal signal states using trace buffers. Hardware assertions are promising to improve observability during post-silicon debug. Unfortunately, we cannot synthesize thousands (or millions) of pre-silicon assertions as hardware checkers (coverage monitors) due to hardware overhead constraints. Therefore, we need to select the most profitable assertions based on design constraints. However, the design constraints can also change dynamically during the device lifetime due to changes in use-case scenarios as well as input variations. Therefore, assertion selection needs to dynamically adapt based on changing circumstances. In this article, we propose an assertion-based post-silicon validation framework to address the above challenges. Specifically, this article makes two important contributions. We propose a clustering-based assertion selection technique that can select the most profitable pre-silicon assertions to maximize the fault coverage. We also present a cost-aware dynamic refinement technique that can select beneficial hardware checkers during runtime based on changing design constraints. Experimental evaluation demonstrates that our proposed pre-silicon assertion selection can outperform state-of-the-art assertion ranking methods (Goldmine and HARM). The results also highlight that our proposed post-silicon dynamic refinement can accurately predict area (less than 5% error) and power consumption (less than 3% error) of hardware checkers at runtime. This accurate prediction enables the identification of the most profitable hardware checkers based on design constraints. 

Concolic testing is a scalable solution for automated generation of directed tests for validation of hardware designs. Unfortunately, concolic testing fails to cover complex corner cases such as hard-to-activate branches. In this article, we propose an incremental concolic testing technique to cover hard-to-activate branches in register-transfer level (RTL) models. We show that a complex branch condition can be viewed as a sequence of easy-to-activate events. We map the branch coverage problem to the coverage of a sequence of events. We propose an efficient algorithm to cover the sequence of events using concolic testing. Specifically, the test generated to activate the current event is used as the starting point to activate the next event in the sequence. Experimental results demonstrate that our approach can be used to generate directed tests to cover complex corner cases in RTL models while state-of-the-art methods fail to activate them. 

System-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions. 

Hardware verification of modern electronic systems has been identified as a major bottleneck due to the increasing complexity and time-to-market constraints. One of the major objectives in hardware verification is to drastically reduce the validation and debug time without sacrificing the design quality. Assertion-based verification is a promising avenue for efficient hardware validation and debug. In this paper, we provide a comprehensive survey of recent progress in assertion-based hardware verification. Specifically, we outline how to define assertions using temporal logic to specify expected behaviors in different abstraction levels. Next, we describe state-of-the art approaches for automated generation of assertions. We also discuss test generation techniques for activating assertions to ensure that the generated assertions are valid. Finally, we present both pre-silicon and post-silicon assertion-based validation approaches that utilize simulation, formal methods as well as hybrid techniques. We conclude with a discussion on utilizing assertions for verifying both functional and non-functional requirements. 

Assertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously.